(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 128))
(declare-fun v1 () (_ BitVec 54))
(declare-fun v2 () (_ BitVec 103))
(declare-fun v3 () (_ BitVec 119))
(declare-fun v4 () (_ BitVec 35))
(assert (let ((e5(_ bv65695061716 36)))
(let ((e6 (ite (bvugt ((_ sign_extend 9) v3) v0) (_ bv1 1) (_ bv0 1))))
(let ((e7 (bvsub v0 ((_ zero_extend 93) v4))))
(let ((e8 (bvadd v0 v0)))
(let ((e9 (bvneg v1)))
(let ((e10 (bvurem ((_ zero_extend 9) v3) e8)))
(let ((e11 ((_ zero_extend 1) e7)))
(let ((e12 (bvand ((_ sign_extend 9) v3) e8)))
(let ((e13 (bvcomp e7 ((_ zero_extend 127) e6))))
(let ((e14 (bvor v1 ((_ zero_extend 53) e6))))
(let ((e15 (bvnor e7 v0)))
(let ((e16 (ite (bvuge e7 ((_ zero_extend 74) v1)) (_ bv1 1) (_ bv0 1))))
(let ((e17 (ite (= (_ bv1 1) ((_ extract 79 79) e10)) ((_ zero_extend 34) e16) v4)))
(let ((e18 (bvlshr e15 ((_ sign_extend 74) e14))))
(let ((e19 (ite (bvuge e9 ((_ zero_extend 53) e13)) (_ bv1 1) (_ bv0 1))))
(let ((e20 ((_ rotate_left 94) v2)))
(let ((e21 (bvmul v0 e8)))
(let ((e22 ((_ rotate_left 6) e7)))
(let ((e23 ((_ zero_extend 26) e14)))
(let ((e24 (ite (= e16 e16) (_ bv1 1) (_ bv0 1))))
(let ((e25 (ite (= ((_ sign_extend 25) e20) e21) (_ bv1 1) (_ bv0 1))))
(let ((e26 (ite (bvugt ((_ zero_extend 53) e25) e9) (_ bv1 1) (_ bv0 1))))
(let ((e27 (ite (bvult v3 ((_ sign_extend 118) e19)) (_ bv1 1) (_ bv0 1))))
(let ((e28 (bvnor ((_ sign_extend 1) e15) e11)))
(let ((e29 ((_ rotate_right 56) e8)))
(let ((e30 (bvurem e16 e6)))
(let ((e31 (ite (= (_ bv1 1) ((_ extract 79 79) e8)) e25 e25)))
(let ((e32 (ite (bvsgt ((_ zero_extend 102) e24) v2) (_ bv1 1) (_ bv0 1))))
(let ((e33 (bvsdiv ((_ zero_extend 25) e20) v0)))
(let ((e34 ((_ extract 60 31) e29)))
(let ((e35 (bvshl ((_ zero_extend 75) v1) e11)))
(let ((e36 ((_ rotate_left 0) e30)))
(let ((e37 (bvand ((_ zero_extend 1) v4) e5)))
(let ((e38 (bvule ((_ zero_extend 35) e31) e5)))
(let ((e39 (bvsle ((_ zero_extend 92) e5) e33)))
(let ((e40 (bvugt e13 e32)))
(let ((e41 (bvugt ((_ sign_extend 34) e6) v4)))
(let ((e42 (distinct ((_ sign_extend 92) e5) e29)))
(let ((e43 (distinct v0 ((_ sign_extend 25) v2))))
(let ((e44 (bvule e8 ((_ zero_extend 127) e24))))
(let ((e45 (bvsle ((_ zero_extend 127) e19) e12)))
(let ((e46 (bvuge e13 e16)))
(let ((e47 (bvuge v0 ((_ sign_extend 92) e37))))
(let ((e48 (bvugt ((_ zero_extend 19) v4) v1)))
(let ((e49 (bvuge e33 e7)))
(let ((e50 (bvult e8 e21)))
(let ((e51 (= e6 e25)))
(let ((e52 (bvsge e29 ((_ zero_extend 127) e19))))
(let ((e53 (bvsge ((_ sign_extend 18) e37) e14)))
(let ((e54 (bvule e12 e7)))
(let ((e55 (distinct e20 ((_ zero_extend 102) e30))))
(let ((e56 (bvsle e17 ((_ zero_extend 34) e30))))
(let ((e57 (bvsle ((_ sign_extend 127) e24) e22)))
(let ((e58 (bvugt e19 e13)))
(let ((e59 (bvsge e34 ((_ zero_extend 29) e31))))
(let ((e60 (bvult ((_ sign_extend 92) e5) e29)))
(let ((e61 (bvule e11 e28)))
(let ((e62 (bvslt ((_ zero_extend 9) v3) e21)))
(let ((e63 (bvuge v3 ((_ zero_extend 118) e24))))
(let ((e64 (bvule v0 e8)))
(let ((e65 (bvult e37 ((_ zero_extend 35) e6))))
(let ((e66 (distinct ((_ zero_extend 1) e8) e11)))
(let ((e67 (distinct v1 ((_ sign_extend 53) e30))))
(let ((e68 (bvugt e9 ((_ zero_extend 53) e27))))
(let ((e69 (bvsle e18 ((_ zero_extend 74) v1))))
(let ((e70 (bvsle e22 ((_ sign_extend 127) e16))))
(let ((e71 (bvsle e10 ((_ zero_extend 127) e32))))
(let ((e72 (bvsge ((_ zero_extend 24) e34) v1)))
(let ((e73 (bvuge ((_ zero_extend 127) e13) e7)))
(let ((e74 (= e35 ((_ zero_extend 1) e33))))
(let ((e75 (distinct v0 ((_ sign_extend 74) e9))))
(let ((e76 (bvslt v3 ((_ zero_extend 118) e6))))
(let ((e77 (bvule e37 e5)))
(let ((e78 (bvslt e35 ((_ zero_extend 128) e6))))
(let ((e79 (= e29 ((_ zero_extend 92) e5))))
(let ((e80 (bvult ((_ zero_extend 79) e27) e23)))
(let ((e81 (bvult e10 e33)))
(let ((e82 (bvsle ((_ zero_extend 1) v0) e11)))
(let ((e83 (bvule e10 ((_ sign_extend 9) v3))))
(let ((e84 (bvslt e10 ((_ zero_extend 127) e26))))
(let ((e85 (bvult v1 ((_ zero_extend 18) e5))))
(let ((e86 (bvuge e11 ((_ zero_extend 10) v3))))
(let ((e87 (bvsgt e22 e12)))
(let ((e88 (bvugt ((_ zero_extend 67) e37) v2)))
(let ((e89 (bvsgt e21 ((_ zero_extend 127) e6))))
(let ((e90 (bvuge e33 ((_ sign_extend 127) e26))))
(let ((e91 (distinct ((_ zero_extend 127) e36) e12)))
(let ((e92 (bvsge e15 ((_ sign_extend 25) e20))))
(let ((e93 (not e43)))
(let ((e94 (=> e65 e71)))
(let ((e95 (not e68)))
(let ((e96 (not e86)))
(let ((e97 (and e38 e69)))
(let ((e98 (= e62 e83)))
(let ((e99 (= e53 e61)))
(let ((e100 (= e47 e97)))
(let ((e101 (= e54 e80)))
(let ((e102 (=> e45 e88)))
(let ((e103 (= e93 e67)))
(let ((e104 (not e84)))
(let ((e105 (xor e63 e52)))
(let ((e106 (not e60)))
(let ((e107 (= e82 e98)))
(let ((e108 (or e42 e104)))
(let ((e109 (= e41 e101)))
(let ((e110 (or e99 e76)))
(let ((e111 (not e59)))
(let ((e112 (and e57 e103)))
(let ((e113 (or e100 e56)))
(let ((e114 (ite e94 e96 e109)))
(let ((e115 (not e77)))
(let ((e116 (or e46 e106)))
(let ((e117 (= e72 e66)))
(let ((e118 (and e110 e95)))
(let ((e119 (ite e114 e50 e81)))
(let ((e120 (not e118)))
(let ((e121 (or e58 e105)))
(let ((e122 (not e39)))
(let ((e123 (not e85)))
(let ((e124 (or e87 e123)))
(let ((e125 (= e108 e115)))
(let ((e126 (=> e102 e120)))
(let ((e127 (=> e91 e124)))
(let ((e128 (or e113 e126)))
(let ((e129 (=> e89 e112)))
(let ((e130 (and e74 e55)))
(let ((e131 (not e64)))
(let ((e132 (ite e51 e107 e40)))
(let ((e133 (not e73)))
(let ((e134 (=> e75 e133)))
(let ((e135 (and e111 e90)))
(let ((e136 (=> e78 e92)))
(let ((e137 (and e125 e134)))
(let ((e138 (=> e137 e128)))
(let ((e139 (xor e117 e117)))
(let ((e140 (=> e44 e70)))
(let ((e141 (or e127 e119)))
(let ((e142 (=> e79 e136)))
(let ((e143 (xor e141 e141)))
(let ((e144 (not e140)))
(let ((e145 (xor e129 e138)))
(let ((e146 (xor e116 e122)))
(let ((e147 (or e135 e143)))
(let ((e148 (not e131)))
(let ((e149 (=> e144 e146)))
(let ((e150 (=> e148 e148)))
(let ((e151 (xor e48 e145)))
(let ((e152 (not e130)))
(let ((e153 (or e152 e142)))
(let ((e154 (or e139 e150)))
(let ((e155 (=> e121 e132)))
(let ((e156 (not e155)))
(let ((e157 (=> e149 e156)))
(let ((e158 (= e151 e49)))
(let ((e159 (=> e147 e147)))
(let ((e160 (=> e157 e157)))
(let ((e161 (=> e159 e158)))
(let ((e162 (= e153 e160)))
(let ((e163 (and e154 e162)))
(let ((e164 (=> e163 e161)))
(let ((e165 (and e164 (not (= v0 (_ bv0 128))))))
(let ((e166 (and e165 (not (= v0 (bvnot (_ bv0 128)))))))
(let ((e167 (and e166 (not (= e6 (_ bv0 1))))))
(let ((e168 (and e167 (not (= e8 (_ bv0 128))))))
e168
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
